es:ES, ff:FIFO. ff.Receiver  j,i:ff.C{e:E| ff.S(j,i,e)} {e:E| ff.R(i,e)}  

latex

Definitions	x:A. B(x), t  T, ff.Receiver, , x. t(x), x:A. B(x), x(s)
Lemmas	pi1 wf, fifoC wf, es-E wf, fifoS wf, fifoR wf, fifoSender wf, event system wf, FIFO wf